\begin{tabbing}
$\forall$$T$:Type, $L_{1}$, $L_{2}$:$T$ List, $i$, $j$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{1}$$\parallel$}}$.
\\[0ex]$L_{2}$ $=$ swap($L_{1}$;$i$;$j$)
\\[0ex]$\Rightarrow$ \{\=$L_{2}$[$i$] $=$ $L_{1}$[$j$] $\in$ $T$ \& $L_{2}$[$j$] $=$ $L_{1}$[$i$] $\in$ $T$ \& $\parallel$$L_{2}$$\parallel$ $=$ $\parallel$$L_{1}$$\parallel$ $\in$ $\mathbb{Z}$ \& $L_{1}$ $=$ swap($L_{2}$;$i$;$j$)\+
\\[0ex]\& ($\forall$$x$:$\mathbb{N}$$_{\mbox{\scriptsize $<\parallel$$L_{2}$$\parallel$}}$. $\neg$$x$ $=$ $i$ $\in$ $\mathbb{Z}$ $\Rightarrow$ $\neg$$x$ $=$ $j$ $\in$ $\mathbb{Z}$ $\Rightarrow$ $L_{2}$[$x$] $=$ $L_{1}$[$x$] $\in$ $T$)\}
\-
\end{tabbing}